M:MsgA, a:Id. a declared in M   

latex

Definitions	x:A. B(x), t  T, , a declared in M, t.1, t.2, x. t(x), MsgA, x(s)
Lemmas	assert wf, fpf-dom wf, Knd wf, Kind-deq wf, fpf-trivial-subtype-top, locl wf, Id wf, msga wf